Nuprl Definition : p-open
11,40
postcript
pdf
p-open(
p
)
== {
C
:(
n
:
({0..
n
}
Outcome))
{0..2
}|
== {
s
:(
Outcome),
j
:
,
i
:{0..
j
}. (
C
(<
i
,
s
>))
(
C
(<
j
,
s
>))}
latex
clarification:
p-open(
p
)
== {
C
:(
n
:
({0..
n
}
p-outcome(
p
)))
{0..2
}|
== {
s
:(
p-outcome(
p
)),
j
:
,
i
:{0..
j
}. (
C
(<
i
,
s
>))
(
C
(<
j
,
s
>))}
latex
Definitions
{
x
:
A
|
B
(
x
)}
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
Outcome
,
,
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
#$n
,
A
B
,
f
(
a
)
,
<
a
,
b
>
FDL editor aliases
p-open
origin